Inference at * 
Iof proof for Lemma p-fun-exp-injection:


  A:Type, f:(A(A + Top)). p-inject(A;A;f)  (n:. p-inject(A;A;f^n)) 

latex

 by ((InductionOnNat) 
CollapseTHEN (Auto)) 

latex

C1: .....basecase..... NILNIL

C1: 1. A : Type
C1: 2. f : A(A + Top)
C1: 3. p-inject(A;A;f)
C1:   p-inject(A;A;f^0)
C2: .....upcase..... NILNIL

C2: 1. A : Type
C2: 2. f : A(A + Top)
C2: 3. p-inject(A;A;f)
C2: 4. n : 
C2: 5. 0 < n
C2: 6. p-inject(A;A;f^n - 1)
C2:   p-inject(A;A;f^n)
C.

Definitions	Void, n+m, -n, A, False, i  j , A  B, {x:A| B(x)} , left + right, Top, P  Q, x:A. B(x), , t  T, s = t, n - m, #$n, f^n, a < b, , x:AB(x), Type, p-inject(A;B;f)
Lemmas	ge wf, nat properties, top wf, nat wf, nat ind tp, p-inject wf